Require Import Arith.
Require Import AutoSep.
Set Implicit Arguments.

(* ============================================================================
 * natural number lemmas
 * ========================================================================= *)

Lemma factor_pow2 : forall n, exists a b, (b < pow2 32)%nat /\ n = a * pow2 32 + b.
  induction n.
  exists 0.
  exists 0.
  auto.
  destruct IHn.
  destruct H.
  destruct (eq_nat_dec (S x0) (pow2 32)).
  exists (S x).
  exists 0.
  destruct H.
  rewrite H0.
  split; [auto | ].
  rewrite mult_succ_l.
  rewrite <- e at 3.
  rewrite plus_n_Sm.
  auto.
  exists x.
  exists (S x0).
  split; [auto | ].
  destruct H.
  rewrite H0.
  rewrite plus_n_Sm.
  auto.
Qed.

(* ============================================================================
 * N lemmas
 * ========================================================================= *)

Lemma Nlt_in': forall n m:nat, (n < m)%nat -> (N.of_nat n < N.of_nat m)%N.
  intros.
  rewrite <- (Nat2N.id n) in H.
  rewrite <- (Nat2N.id m) in H.
  generalize H; clear H.
  generalize (N.of_nat n); intro n'.
  generalize (N.of_nat m); intro m'.
  intro H'.
  apply Nlt_in; assumption.
Qed.

Lemma Nlt_out': forall n m, (N.of_nat n < N.of_nat m)%N -> (n < m)%nat.
  intros.
  rewrite <- (Nat2N.id n).
  rewrite <- (Nat2N.id m).
  generalize H.
  generalize (N.of_nat n); intro n'.
  generalize (N.of_nat m); intro m'.
  intro H'.
  apply Nlt_out; assumption.
Qed.

Lemma Npow2_of_nat_pow2 : forall n, Npow2 n = N.of_nat (pow2 n).
  intro.
  induction n; auto.
  replace (Npow2 (S n)) with (Npow2 n + Npow2 n)%N.
  simpl.
  replace (pow2 n + 0) with (pow2 n).
  rewrite Nat2N.inj_add.
  rewrite <- IHn.
  auto.
  auto.
  assert (Npow2 (S n) = 2 * Npow2 n)%N.
  auto.
  rewrite H.
  assert (2 = N.succ (N.succ 0))%N by auto.
  rewrite H0.
  rewrite N.mul_succ_l.
  assert (N.succ 0 * Npow2 n = Npow2 n)%N.
    rewrite N.mul_succ_l.
    simpl; auto.
  rewrite H1.
  auto.
Qed.

Lemma bound_N_nat' : forall sz n, (n < pow2 sz)%nat -> (N.of_nat n < Npow2 sz)%N.
  intros.
  rewrite Npow2_of_nat_pow2.
  apply Nlt_in'; auto.
Qed.


(* ============================================================================
 * nat to word
 * ========================================================================= *)
Lemma wlt_goodSize : forall n m:nat, goodSize n -> goodSize m ->
                                     natToW n < natToW m -> (n < m)%nat.
  unfold goodSize, natToW.
  intros.
  generalize dependent 32.
  intros.
  Hint Rewrite (*Npow2_nat*) wordToN_nat : N.
  pre_nomega.
  assumption.
Qed.

Lemma natToWord_pow2' : forall(sz k:nat)(w:word sz),
                          natToWord sz (k * pow2 sz) ^+ w = w.
  induction k.
  intro.
  replace (0 * pow2 sz) with 0.
  apply wplus_unit.
  words.
  rewrite mult_succ_l.
  rewrite natToWord_plus.
  intro.
  rewrite <- wplus_assoc.
  rewrite natToWord_pow2.
  rewrite wplus_unit.
  apply IHk.
Qed.

Lemma natToWord_pow2_zero: forall sz n, $ (n * pow2 sz) = natToWord sz 0.
  intros.
  rewrite <- (wplus_unit $(n * pow2 sz)).
  rewrite wplus_comm.
  apply natToWord_pow2'.
Qed.

Lemma natToWord_pow2_factor : forall (sz:nat)(w:word sz), exists n, forall k,
                    (n < pow2 sz)%nat /\ w = natToWord sz (k * pow2 sz + n).
  intros.
  exists (wordToNat w).
  intro.
  split.
  apply (wordToNat_bound w).
  rewrite natToWord_plus.
  rewrite natToWord_pow2'.
  rewrite natToWord_wordToNat.
  reflexivity.
Qed.

Corollary natToWord_pow2_factor' : forall (sz:nat)(w:word sz), exists n,
                    (n < pow2 sz)%nat /\ w = natToWord sz n.
  intros.
  generalize natToWord_pow2_factor; intro.
  specialize (H sz w).
  destruct H.
  specialize (H 0).
  destruct H.
  simpl in H0.
  exists x; auto.
Qed.

(* contrapositive of natToWord_injective *)
Theorem natToWord_inj' : forall sz x y,
                               (x < pow2 sz)%nat -> (y < pow2 sz)%nat ->
                               x <> y ->
                               natToWord sz x <> natToWord sz y.
  intros.
  red; intro.
  apply natToWord_inj in H2; auto.
Qed.
  
Theorem wlt_natToWord_mono : forall sz x y:nat,
                               (x < pow2 sz)%nat -> (y < pow2 sz)%nat ->
                               (x < y)%nat -> natToWord sz x < natToWord sz y.
  intros.
  pre_nomega.
  repeat rewrite wordToNat_natToWord_idempotent; auto.
  apply bound_N_nat'; auto.
  apply bound_N_nat'; auto.
Qed.

Theorem wlt_natToWord_pres : forall sz x y:nat,
                               (x < pow2 sz)%nat -> (y < pow2 sz)%nat ->
                               natToWord sz x < natToWord sz y -> (x < y)%nat.
  intros.
  pre_nomega.
  rewrite wordToNat_natToWord_idempotent in H1.
  rewrite wordToNat_natToWord_idempotent in H1.
  auto.
  apply bound_N_nat'; auto.
  apply bound_N_nat'; auto.
Qed.

Theorem wle_natToWord_mono : forall sz x y:nat,
                               (x < pow2 sz)%nat -> (y < pow2 sz)%nat ->
                               (x <= y)%nat -> natToWord sz x <= natToWord sz y.
  intros.
  pre_nomega.
  repeat rewrite wordToNat_natToWord_idempotent; auto.
  apply bound_N_nat'; auto.
  apply bound_N_nat'; auto.
Qed.

Theorem wle_natToWord_pres : forall sz x y:nat,
                               (x < pow2 sz)%nat -> (y < pow2 sz)%nat ->
                               natToWord sz x <= natToWord sz y -> (x <= y)%nat.
  intros.
  pre_nomega.
  rewrite wordToNat_natToWord_idempotent in H1.
  rewrite wordToNat_natToWord_idempotent in H1.
  auto.
  apply bound_N_nat'; auto.
  apply bound_N_nat'; auto.
Qed.


(* ============================================================================
 * word to nat
 * ========================================================================= *)

Corollary roundTrip : forall sz n : nat,
                       (n < pow2 sz)%nat -> wordToNat (natToWord sz n) = n.
  intros.
  apply wordToNat_natToWord_idempotent.
  apply bound_N_nat'.
  auto.
Qed.

Ltac destruct_word sz w n :=
  let H := fresh "W" in
  assert (H:exists w', (w' < pow2 sz)%nat /\ w = natToWord sz w') by
      apply natToWord_pow2_factor';
  elim H; clear H; intros n H; destruct H; subst.

Ltac destruct_W w n := destruct_word 32 w n.

(* injectivity of wordToNat *)
Theorem wordToNat_inj : forall sz (x y:word sz),
                          wordToNat x = wordToNat y -> x = y.
  intros.
  destruct_word sz x x'.
  destruct_word sz y y'.
  do 2 (rewrite roundTrip in H; auto).
Qed.

Theorem wordToNat_inj' : forall sz (x y:word sz), x <> y ->
                                                      wordToNat x <> wordToNat y.
  intros.
  destruct_word sz x x'.
  destruct_word sz y y'.
  do 2 (rewrite roundTrip; auto).
Qed.


(* ============================================================================
 * word arithmetic
 * ========================================================================= *)

Lemma W_le_lt_trans : forall i j s : W, i <= j -> j < s -> i < s.
  intros.
  nomega.
Qed.

Lemma wordToNat_wminus : forall n m:W, n <= m ->
                              wordToNat (m ^- n) = wordToNat m - wordToNat n.
  intros.
  pre_nomega.
  unfold wminus.
  assert (exists n', forall k, (n' < pow2 32)%nat /\ n = natToW (k*pow2 32 + n')) by apply natToWord_pow2_factor.
  assert (exists m', forall k, (m' < pow2 32)%nat /\ m = natToW (k*pow2 32 + m')) by apply natToWord_pow2_factor.
  destruct H0.
  destruct H1.
  specialize (H0 0).
  destruct H0.
  specialize (H1 0).
  destruct H1.
  simpl in H2.
  simpl in H3.
  subst.

  unfold wneg.
  rewrite NToWord_nat.
  rewrite N2Nat.inj_sub.
  rewrite Npow2_nat.
  
  rewrite natToWordToN.
  rewrite Nat2N.id.
  unfold natToW.

  rewrite <- natToWord_plus.
  rewrite NPeano.Nat.add_sub_assoc.
  rewrite plus_comm.
  rewrite <- NPeano.Nat.add_sub_assoc.

  assert (natToW (pow2 32 + (x0 - x)) = (natToW (x0 - x))).
    unfold natToW.
    rewrite natToWord_plus.
    rewrite natToWord_pow2.
    rewrite wplus_unit.
    auto.
  unfold natToW in H2.
  rewrite H2.

  repeat rewrite wordToNat_natToWord_idempotent; auto.
  unfold natToW in *.
  do 2 rewrite wordToNat_natToWord_idempotent in H.
  auto.
  apply bound_N_nat; auto.
  apply bound_N_nat; auto.
  apply bound_N_nat; auto.
  apply lt_le_weak.
  auto.
  apply bound_N_nat; auto.
Qed.

(* not used
Lemma Nlt_wordToN_wordToNat : forall n m:W, (wordToN n < wordToN m)%N ->
                                            (wordToNat n < wordToNat m)%nat.
  intros.
  repeat rewrite wordToN_nat in H.
  generalize H; clear H.
  generalize (wordToNat n); intro n'.
  generalize (wordToNat m); intro m'.
  intro.
  apply Nlt_out'; assumption.
Qed.*)

Lemma wlt_wminus_one : forall w:W, natToW 0 < w -> w ^- natToW 1 < w.
  intros.
  rewrite <- (natToWord_wordToNat w) at 1.
  rewrite <- (natToWord_wordToNat w) at 2.
  unfold natToW.
  rewrite <- natToW_minus.
  unfold natToW.
  generalize (goodSize_wordToNat w).
  assert (wordToNat w > 0)%nat.
    unfold wlt in H.
    unfold natToW in H.
    rewrite natToWordToN in H.
    rewrite wordToN_nat in H.
    change (0 < wordToNat w)%nat.
    apply Nlt_out'; assumption.
  apply bound_N_nat; auto.
 
  generalize H0.
  generalize (wordToNat w).
  induction n.
  intros; omega.
  intros.
  assert (H3: S n - 1 = n) by (induction n; auto); rewrite H3.
  unfold wlt.
  do 2 (rewrite wordToN_nat).
  rewrite wordToNat_natToWord_idempotent.
  rewrite wordToNat_natToWord_idempotent.
  apply Nlt_in'; auto.
  auto.
  apply goodSize_S; auto.
  change (0 < wordToNat w)%nat.
  unfold wlt in H.
  do 2 (rewrite wordToN_nat in H).
  apply Nlt_out'; assumption.
Qed.

Lemma S_wminus_one_id : forall w:W, natToW 0 < w ->
                              S (wordToNat (w ^- natToW 1)) = wordToNat w.
  intros.
  rewrite wordToNat_wminus.
  rewrite roundTrip_1.
  assert (wordToNat w > 0)%nat.
    unfold wlt in H.
    unfold natToW in H.
    rewrite natToWordToN in H.
    rewrite wordToN_nat in H.
    change (0 < wordToNat w)%nat.
    apply Nlt_out'; assumption.
    apply bound_N_nat; auto.

  generalize H0.
  generalize (wordToNat w).
  induction n.
  intros; omega.
  intros.
  assert (H3: S n - 1 = n) by (induction n; auto); rewrite H3; auto.

  unfold wlt in H.
  do 2 (rewrite wordToN_nat in H).
  apply Nlt_out' in H.

  unfold wlt.
  do 2 (rewrite wordToN_nat).
  intro.
  apply Nlt_out' in H0.
  rewrite roundTrip_0 in *.
  rewrite roundTrip_1 in *.
  intuition.
Qed.

Lemma wlt_natToWord_zero_minus_1 : forall n, natToW 0 < natToW n ->
                                             natToW (n - 1) < natToW n.
  intro n.
  assert (exists a b, (b < pow2 32)%nat /\ n = a * pow2 32 + b) by apply factor_pow2.
  elim H; clear H; intros a H.
  elim H; clear H; intros b H.
  destruct H.
  rewrite H0.
  destruct b.
  intro.
  elimtype False.

  rewrite natToW_plus in H1.
  unfold natToW in *.
  rewrite natToWord_pow2_zero in H1.
  rewrite wplus_unit in H1.
  unfold wlt in H1.
  rewrite natToWordToN in H1.
  apply (Nlt_irrefl' (N.of_nat 0)); assumption.
  auto.
  intro.
  unfold natToW.
  assert (forall n, n + S b -1 = n + b).
    induction n0; simpl; auto.
    induction b; auto.
    assert (S (n0 + b) = n0 + S b) by auto.
    rewrite H2.
    apply NPeano.Nat.sub_0_r.
  rewrite H2.
  repeat rewrite natToWord_plus.
  repeat rewrite natToWord_pow2'.
  repeat rewrite wplus_unit.
  unfold wlt.
  repeat rewrite natToWordToN.
  apply Nlt_in'; auto.
  apply bound_N_nat; assumption.
  apply bound_N_nat.
  auto.
Qed.

Lemma W_zero_le : forall w:W, natToW 0 <= w.
  intros.
  pre_nomega.
  rewrite roundTrip_0.
  omega.
Qed.

Hint Resolve W_zero_le.

Lemma W_neq_zero_lt : forall w:W, w <> natToW 0 -> natToW 0 < w.
  intros.
  pre_nomega.
  (*reduce_words*)
  rewrite roundTrip_0.
  red in H.
  assert (forall w:W, (wordToNat w = 0)%nat -> w = 0).
    intros.
    replace w0 with (natToW (wordToNat w0)).
    rewrite H0; reflexivity.
    apply natToWord_wordToNat.
    assert (wordToNat w = 0 -> False).
      intro.
      apply H0 in H1.
      auto.
    generalize H1.
    generalize (wordToNat w) .
    auto.
Qed.

Hint Resolve W_neq_zero_lt.

Corollary wordToNat_wplus_one : forall sz n:nat, (S n < pow2 sz)%nat  ->
                              wordToNat (natToWord sz n ^+ natToWord sz 1) = S n.
  intros.
  rewrite wplus_comm.
  rewrite <- natToWord_S.
  apply roundTrip; auto.
Qed.

Corollary wordToNat_wplus_one_W : forall n m:W, n < m ->
                              wordToNat (n ^+ natToW 1) = S (wordToNat n).
  intros.
  pre_nomega.
 
  assert (exists n', forall k, (n' < pow2 32)%nat /\ n = natToW (k*pow2 32 + n')) by apply natToWord_pow2_factor.
  destruct H0.
  specialize (H0 0).
  destruct H0.
  simpl in H1.
  subst.
  
  unfold natToW.
  rewrite roundTrip.
  apply wordToNat_wplus_one.

  unfold natToW in H.
  rewrite roundTrip in H.
  assert (wordToNat m < pow2 32)%nat by apply wordToNat_bound.
  apply lt_le_S in H.
  eapply le_lt_trans; auto.
  auto.
  auto.
Qed.

Corollary wordToNat_wplus : forall sz x y:nat, (x + y < pow2 sz)%nat ->
                        wordToNat (natToWord sz x ^+ natToWord sz y) = x + y.
  intros.
  rewrite <- natToWord_plus.
  apply roundTrip.
  auto.
Qed.

Corollary wordToNat_wplus_one_W' : forall x y:W, x < y -> wordToNat (x ^+ natToW 1) = (wordToNat x + 1).
  intros.
  rewrite <- plus_n_Sm.
  rewrite plus_0_r.
  eapply wordToNat_wplus_one_W.
  apply H.
Qed.

Theorem wlt_plus_one_mono : forall z x y:W, y < z -> x < y -> x ^+ natToW 1 < y ^+ natToW 1.
  intros.
  pre_nomega.
  repeat erewrite wordToNat_wplus_one_W'.
  nomega.
  pre_nomega; apply H.
  pre_nomega; apply H0.
Qed. 

Theorem wle_wplus_one_mono : forall x y z:W, y < z -> x <= y ->
                                         x ^+ natToW 1 <= y ^+ natToW 1.
  intros.
  destruct_W x x'.
  destruct_W y y'.
  case_eq (eq_nat_dec x' y'); intros.
  apply eq_le.
  rewrite e.
  auto.

  apply lt_le.
  eapply wlt_plus_one_mono.
  apply H.
  apply le_neq_lt; auto.
  apply natToWord_inj'; auto.
Qed.


(* ============================================================================
 * Tactics
 * ========================================================================= *)
Ltac lift_words :=
  repeat (
    match goal with
      (* avoid looping *)
      | [ H: (natToWord _ _) = (natToWord _ _) |- _ ] => fail
      | [ H: (natToW _ _) = (natToW _ _) |- _ ] => fail
      | [ H: (natToWord _ _) = (natToW _ _) |- _ ] => fail
      | [ H: (natToW _ _) = (natToWord _ _) |- _ ] => fail

      | [ H: ?W = (natToWord _ ?N) |- context [ ?W ] ] => rewrite H
      | [ H: (natToWord _ ?N) = ?W |- context [ ?W ] ] => rewrite <- H
      | [ H: ?W = (natToW ?N) |- context [ ?W ] ] => rewrite H
      | [ H: (natToW ?N) = ?W |- context [ ?W ] ] => rewrite <- H

      | [ H: ?W = (natToWord _ ?N), H': context [ ?W ] |- _ ] => rewrite H in H'
      | [ H: (natToWord _ ?N) = ?W, H': context [ ?W ] |- _ ] => rewrite <- H in H'
      | [ H: ?W = (natToW ?N), H': context [ ?W ] |- _ ] => rewrite H in H'
      | [ H: (natToW ?N) = ?W, H': context [ ?W ] |- _ ] => rewrite <- H in H'
    end
  ).

(* Now, use rewrite hint
Ltac reduce_words :=
  repeat (
    match goal with
      | [ H: context [ natToWord _ (wordToNat ?W) ] |- _ ] =>
        rewrite natToWord_wordToNat in H
      | [ H: context [ natToW (wordToNat ?W) ] |- _ ] =>
        rewrite natToWord_wordToNat in H

      | [ |- context [ natToWord _ (wordToNat ?W) ] ] =>
        rewrite natToWord_wordToNat
      | [ |- context [ natToW (wordToNat ?W) ] ] =>
        rewrite natToWord_wordToNat

      | [ H: (?N < pow2 ?sz)%nat, H': context [ wordToNat (natToWord ?sz ?N) ]
          |- _ ] =>
        rewrite roundTrip in H'
      | [ H: goodSize ?N, H': context [ wordToNat (natToW ?N) ] |- _ ] =>
        rewrite wordToNat_natToWord_idempotent in H'

      | [ H: context [ wordToNat (natToWord ?sz ?N) ] |- _ ] =>
        assert (N < pow2 sz)%nat by auto; rewrite roundTrip in H
      | [ H: context [ wordToNat (natToW ?N) ] |- _ ] =>
        assert (goodSize N) by auto; rewrite wordToNat_natToWord_idempotent in H

      | [ H: (?N < pow2 ?sz)%nat |- context [ wordToNat (natToWord ?sz ?N) ] ] => rewrite roundTrip
      | [ H: goodSize ?N |- context [ wordToNat (natToW ?N) ] ] => rewrite wordToNat_natToWord_idempotent

      | [ |- context [ wordToNat (natToWord ?sz ?N) ] ] =>
        assert (N < pow2 sz)%nat by auto; rewrite wordToNat_natToWord_idempotent
      | [ |- context [ wordToNat (natToW ?N) ] ] =>
        assert (goodSize N) by auto; rewrite wordToNat_natToWord_idempotent
    end; auto
  ).

Ltac W_lt :=
  match goal with
  | [ |- (natToW 0 <= ?W)%word ] => apply W_zero_le
  | [ H: (natToW 0) < (natToW ?N) |- natToW ?N ^- natToW 1 < natToW ?N ] => apply wlt_wminus_one
  | [ H: not (eq (natToW ?N) (natToW 0)) |- natToW ?N ^- natToW 1 < natToW ?N ] => apply wlt_wminus_one; apply W_neq_zero_lt; assumption
  | [ H: not (eq ?W (natToW 0)) |- natToW 0 < ?W ] => apply W_neq_zero_lt; auto
  end.
*)

(*
Ltac reduce_N :=
  repeat (
    match goal with
      | [ H: ?W = (N.to_nat ?N) |- context [ ?W ] ] => rewrite H
      | [ |- context [ N.of_nat (N.to_nat _ ?N) ] ] => rewrite N2Nat.id
    end
  ); auto.

Ltac goodsize :=
  repeat (
      match goal with
          | [ H: goodSize ?N |- ?N < pow2 32 ] => apply goodSize_danger
          | [ H: goodSize ?N |- N.of_nat ?N < Npow2 32 ] => assumption
          (*| [ H: ?N = wordToN ?sz ?W |- ?N < Npow2 ?sz ] => *)
      end
  ).
*)
